package org.xteam.sled.solver;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import org.xteam.sled.semantic.exp.DefaultExpVisitor;
import org.xteam.sled.semantic.exp.Exp;
import org.xteam.sled.semantic.exp.ExpVar;


public class FreshState {
	private Set<String> original;
	private Map<String, Exp> var2exp = new HashMap<String, Exp>();
	private Map<Exp, String> exp2var = new HashMap<Exp, String>();
	
	public FreshState(Set<String> original) {
		this.original = new HashSet<String>(original);
	}

	public String varFor(Exp expr) {
		String var = exp2var.get(expr);
		if (var != null)
			return var;
		String base = new GetBase().get(expr);
		
		String v = expr instanceof ExpVar ? ((ExpVar) expr).name() : freshVariable(base);
		if (var2exp.get(v) != null)
			throw new RuntimeException("fresh variable already in use");
		var2exp.put(v, expr);
		exp2var.put(expr, v);
		return v;
	}
	
	private String freshVariable(String base) {
		base = baseName(base);
		String name;
		int n = 1;
		do {
			name = base +  "#" + n;
			++n;
		} while (inUse(name));
		return name;
	}

	private boolean inUse(String name) {
		return original.contains(name) || var2exp.containsKey(name);
	}
	
	public boolean isOriginal(String name) {
		return original.contains(name);
	}

	private String baseName(String base) {
		int pos = base.indexOf('#');
		if (pos < 0)
			return base;
		
		for (int i = pos + 1; i < base.length(); ++i) {
			if (! Character.isDigit(base.charAt(i)))
				return base;
		}
		return base.substring(0, pos);
	}

	private static class GetBase extends DefaultExpVisitor {
		String base = "???";
		public void visitVar(ExpVar expVar) {
			base = expVar.name();
		}
		public String get(Exp expr) {
			expr.visit(this);
			return base;
		}
	}

	public Exp var2exp(String name) {
		return var2exp.get(name);
	}
}
